p:(IdLnk List), i, j:Id. lconnects(p;i;j)   

latex

Definitions	x:A. B(x), t  T, , lconnects(p;i;j), P & Q, P  Q, A, ||as||, Y, False, P  Q
Lemmas	lpath wf, length wf1, IdLnk wf, Id wf, not wf, lsrc wf, hd wf, non neg length, ldst wf, last wf, assert of null, assert wf, null wf